\begin{tabbing}
ecl{-}mng\=\{i:l\}\+
\\[0ex](${\it es}$; $i$; ${\it ds}$; ${\it da}$; $x$; ${\it snd}$; ${\it upd}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=l{-}all(msg{-}spec{-}links(${\it snd}$); $l$.ecl{-}mng{-}sends\{i:l\}(${\it es}$; $i$; ${\it ds}$; ${\it da}$; $x$; $l$; ${\it snd}$))\+
\\[0ex]$\wedge$ l{-}all(update{-}spec{-}vars(${\it upd}$); $z$.ecl{-}mng{-}update\{i:l\}(${\it es}$; $i$; ${\it ds}$; ${\it da}$; $x$; $z$; ${\it upd}$))
\-
\end{tabbing}